Simplify executing unfolds and evaluating unfoldings by removing the need to fully produce the predicate body.
The idea (thanks @JonasAlaif!) is to reuse the result of verifying the predicate body's well-definedness: After doing so, we know the potential branches and the potential heaps we get from a predicate unfold. Thus, we can remember these heaps, the assumptions that came with them, as well as the declarations we made in the process, and simply declare them, assume them, and add them to our current heap when we are asked to unfold the predicate.

For now, this optimization is disabled by default, and can be turned on by using the new flag --enableSimplifiedUnfolds.

This requires:

• Using the FunctionRecorder also while verifying a predicate, to collect all relevant declarations. This in turn required moving some code around between FunctionRecorder, FunctionData, and FunctionVerificationUnit, since the FunctionRecorder is now no longer only used for functions.
• Storing a tree structure containing all heaps etc. under the respective branch conditions resulting from inhaling a predicate body after verifying the predicate
• Adjusting the assumptions and heap chunks when doing the unfold (e.g., scaling permission amounts, replacing the snapshots with the actual snapshot of the unfolded predicate, and turning ordinary chunks into QP chunks)
• Recording some additional information in the FunctionRecorder that was not previously required, like apparently permission maps.